To tackle the increasing complexity of digital electronic circuits, designers need faster and more accurate methods for verifying the functionality of such circuits, particularly in light of ever shrinking product development times.
The complexity of designing such circuits is often handled by expressing the design in a high-level hardware description language (HLHDL), such as Verilog HDL. The detailed syntax and semantics of Verilog HDL is specified in the following publication that is herein incorporated by reference: “IEEE Standard Hardware Description Language Based on the Verilog Hardware Description Language,” IEEE Standard 1364-1995, Institute of Electrical and Electronic Engineers, Oct. 1996.
HLHDLs allow the designer to save design time by permitting him or her to express the desired functionality at the register transfer level (RTL) of abstraction or higher. The high-level HDL description is then converted into an actual circuit through a process, well known to those of ordinary skill in the art as “synthesis,” involving translation and optimization. An HLHDL description can be verified without translating the HLHDL to a lower-level description.
Verification of the HLHDL description is important since detecting a circuit problem early prevents the expenditure of valuable designer time on achieving an efficient circuit implementation for a design which, at a higher level, will not achieve its intended purpose. Such an HLHDL design, whose correctness is to be determined, shall be referred to as the “design under test” or DUT. In addition, testing of the DUT can be accomplished much more quickly in an HLHDL than after the DUT has been translated into a lower-level, more circuit oriented, description.
HLHDLs describe, directly or indirectly, the two main kinds of circuit entities of an RTL circuit description: i) state devices or sequential logic which store data upon application of a clock signal, and ii) combinational logic. The state devices typically act as either: i) an interface between conceptually distinct circuit systems, or ii) storage for the intermediate or final results of functional evaluation performed by the combinational logic.
Conventionally, such a DUT would be tested by simulating it and applying a test stimulus to the simulation. The test stimulus often consists of multiple “stimulus vectors,” each stimulus vector being applied at a succeeding time increment. Each stimulus vector is typically a collection of binary bits, each of which is applied to a corresponding input of the design under test (DUT). The response of the DUT to the test stimulus is collected and analyzed. If the collected response agrees with the expected response then, to some degree of certainty, the DUT is believed by the circuit designer to be expressing the desired functionality. While simulation provides for relatively “deep” penetration of the space of possible states for the DUT (i.e., can transition the DUT through a long sequence of time steps), it often does not provide acceptably broad coverage—i.e., the circuit designer does not know the extent to which the test stimulus has exercised the DUT.
Another approach is the use of exhaustive formal search methods. One application of formal methods involves the definition of a set of erroneous states for the DUT and the determination, by formal methods, as to whether an erroneous state is reachable from an initial state of the DUT. Such methods provide potentially complete (i.e., broad) coverage of the state space of the DUT, but for even moderately complex DUTs the state space is so large that time and resource limits preclude a deep exploration. Therefore, erroneous conditions that require a greater number of state transitions of the DUT before they can be reached will not be identified.
It would therefore be desirable to combine the depth coverage capabilities of simulation with the breadth coverage of formal methods to achieve a verification technique that can more thoroughly test large DUTs.